; COMMAND-LINE: --finite-model-find -q
(set-logic HO_ALL)
(set-info :status sat)
(declare-sort $$unsorted 0)
(declare-sort tptp.poly_p1267267526omplex 0)
(declare-sort tptp.poly_poly_complex 0)
(declare-sort tptp.poly_complex 0)
(declare-sort tptp.poly_nat 0)
(declare-sort tptp.complex 0)
(declare-sort tptp.real 0)
(declare-sort tptp.bool 0)
(declare-sort tptp.nat 0)
(declare-fun tptp.fundam769667258omplex ((-> tptp.complex tptp.complex)) Bool)
(declare-fun tptp.fundam835161864omplex (tptp.poly_complex) tptp.nat)
(declare-fun tptp.plus_plus_complex (tptp.complex tptp.complex) tptp.complex)
(declare-fun tptp.plus_plus_nat (tptp.nat tptp.nat) tptp.nat)
(declare-fun tptp.plus_p1547158847omplex (tptp.poly_complex tptp.poly_complex) tptp.poly_complex)
(declare-fun tptp.plus_p138939463omplex (tptp.poly_poly_complex tptp.poly_poly_complex) tptp.poly_poly_complex)
(declare-fun tptp.zero_zero_complex () tptp.complex)
(declare-fun tptp.zero_zero_nat () tptp.nat)
(declare-fun tptp.zero_z1746442943omplex () tptp.poly_complex)
(declare-fun tptp.zero_zero_poly_nat () tptp.poly_nat)
(declare-fun tptp.zero_z1040703943omplex () tptp.poly_poly_complex)
(declare-fun tptp.zero_z1200043727omplex () tptp.poly_p1267267526omplex)
(declare-fun tptp.ord_less_nat (tptp.nat tptp.nat) Bool)
(declare-fun tptp.ord_less_eq_nat (tptp.nat tptp.nat) Bool)
(declare-fun tptp.ord_less_eq_real (tptp.real tptp.real) Bool)
(declare-fun tptp.poly_complex2 (tptp.poly_complex tptp.complex) tptp.complex)
(declare-fun tptp.poly_nat2 (tptp.poly_nat tptp.nat) tptp.nat)
(declare-fun tptp.poly_poly_complex2 (tptp.poly_poly_complex tptp.poly_complex) tptp.poly_complex)
(declare-fun tptp.poly_p282434315omplex (tptp.poly_p1267267526omplex tptp.poly_poly_complex) tptp.poly_poly_complex)
(declare-fun tptp.real_V638595069omplex (tptp.complex) tptp.real)
(declare-fun tptp.fFalse () tptp.bool)
(declare-fun tptp.fTrue () tptp.bool)
(declare-fun tptp.pp (tptp.bool) Bool)
(declare-fun tptp.a () tptp.complex)
(declare-fun tptp.c () tptp.complex)
(declare-fun tptp.p () tptp.poly_complex)
(declare-fun tptp.pa () tptp.poly_complex)
(declare-fun tptp.q () tptp.poly_complex)
(assert (not (= tptp.a tptp.zero_zero_complex)))
(assert (forall ((X tptp.complex)) (= (@ (@ tptp.poly_complex2 tptp.q) X) (@ (@ tptp.poly_complex2 tptp.pa) (@ (@ tptp.plus_plus_complex tptp.c) X)))))
(assert (not (@ tptp.fundam769667258omplex (@ tptp.poly_complex2 tptp.p))))
(assert (not (= (@ (@ tptp.poly_complex2 tptp.pa) tptp.c) tptp.zero_zero_complex)))
(assert (not (@ tptp.fundam769667258omplex (@ tptp.poly_complex2 tptp.pa))))
(assert (not (= (@ (@ tptp.poly_complex2 tptp.q) tptp.zero_zero_complex) tptp.zero_zero_complex)))
(assert (= (@ (@ tptp.poly_complex2 tptp.pa) tptp.c) (@ (@ tptp.poly_complex2 tptp.q) tptp.zero_zero_complex)))
(assert (= (@ tptp.fundam835161864omplex tptp.q) (@ tptp.fundam835161864omplex tptp.pa)))
(assert (forall ((X2 tptp.poly_poly_complex)) (= (@ (@ tptp.poly_p282434315omplex tptp.zero_z1200043727omplex) X2) tptp.zero_z1040703943omplex)))
(assert (forall ((X2 tptp.nat)) (= (@ (@ tptp.poly_nat2 tptp.zero_zero_poly_nat) X2) tptp.zero_zero_nat)))
(assert (forall ((X2 tptp.poly_complex)) (= (@ (@ tptp.poly_poly_complex2 tptp.zero_z1040703943omplex) X2) tptp.zero_z1746442943omplex)))
(assert (forall ((X2 tptp.complex)) (= (@ (@ tptp.poly_complex2 tptp.zero_z1746442943omplex) X2) tptp.zero_zero_complex)))
(assert (forall ((P tptp.poly_p1267267526omplex)) (= (forall ((X3 tptp.poly_poly_complex)) (= (@ (@ tptp.poly_p282434315omplex P) X3) tptp.zero_z1040703943omplex)) (= P tptp.zero_z1200043727omplex))))
(assert (forall ((P tptp.poly_complex)) (= (forall ((X3 tptp.complex)) (= (@ (@ tptp.poly_complex2 P) X3) tptp.zero_zero_complex)) (= P tptp.zero_z1746442943omplex))))
(assert (forall ((P tptp.poly_poly_complex)) (= (forall ((X3 tptp.poly_complex)) (= (@ (@ tptp.poly_poly_complex2 P) X3) tptp.zero_z1746442943omplex)) (= P tptp.zero_z1040703943omplex))))
(assert (exists ((Q tptp.poly_complex)) (and (= (@ tptp.fundam835161864omplex Q) (@ tptp.fundam835161864omplex tptp.pa)) (forall ((X tptp.complex)) (= (@ (@ tptp.poly_complex2 Q) X) (@ (@ tptp.poly_complex2 tptp.pa) (@ (@ tptp.plus_plus_complex tptp.c) X)))))))
(assert (not (forall ((Q tptp.poly_complex)) (=> (= (@ tptp.fundam835161864omplex Q) (@ tptp.fundam835161864omplex tptp.pa)) (not (forall ((X tptp.complex)) (= (@ (@ tptp.poly_complex2 Q) X) (@ (@ tptp.poly_complex2 tptp.pa) (@ (@ tptp.plus_plus_complex tptp.c) X)))))))))
(assert (not (@ tptp.fundam769667258omplex (@ tptp.poly_complex2 tptp.q))))
(assert (not (@ tptp.fundam769667258omplex (@ tptp.poly_complex2 tptp.q))))
(assert (forall ((P tptp.poly_poly_complex) (Q2 tptp.poly_poly_complex)) (= (= (@ tptp.poly_poly_complex2 P) (@ tptp.poly_poly_complex2 Q2)) (= P Q2))))
(assert (forall ((P tptp.poly_complex) (Q2 tptp.poly_complex)) (= (= (@ tptp.poly_complex2 P) (@ tptp.poly_complex2 Q2)) (= P Q2))))
(assert (forall ((W tptp.complex)) (let ((_let_1 (@ tptp.poly_complex2 tptp.pa))) (@ (@ tptp.ord_less_eq_real (@ tptp.real_V638595069omplex (@ _let_1 tptp.c))) (@ tptp.real_V638595069omplex (@ _let_1 W))))))
(assert (forall ((X2 tptp.poly_poly_complex)) (= (= tptp.zero_z1040703943omplex X2) (= X2 tptp.zero_z1040703943omplex))))
(assert (forall ((X2 tptp.nat)) (= (= tptp.zero_zero_nat X2) (= X2 tptp.zero_zero_nat))))
(assert (forall ((X2 tptp.complex)) (= (= tptp.zero_zero_complex X2) (= X2 tptp.zero_zero_complex))))
(assert (forall ((X2 tptp.poly_complex)) (= (= tptp.zero_z1746442943omplex X2) (= X2 tptp.zero_z1746442943omplex))))
(assert (forall ((W tptp.complex)) (@ (@ tptp.ord_less_eq_real (@ tptp.real_V638595069omplex (@ (@ tptp.poly_complex2 tptp.q) tptp.zero_zero_complex))) (@ tptp.real_V638595069omplex (@ (@ tptp.poly_complex2 tptp.pa) W)))))
(assert (forall ((P tptp.poly_complex)) (=> (@ (@ tptp.ord_less_nat (@ tptp.fundam835161864omplex P)) (@ tptp.fundam835161864omplex tptp.pa)) (=> (not (@ tptp.fundam769667258omplex (@ tptp.poly_complex2 P))) (exists ((Z tptp.complex)) (= (@ (@ tptp.poly_complex2 P) Z) tptp.zero_zero_complex))))))
(assert (forall ((A tptp.poly_complex) (B tptp.poly_complex) (C tptp.poly_complex)) (let ((_let_1 (@ tptp.plus_p1547158847omplex A))) (= (= (@ _let_1 B) (@ _let_1 C)) (= B C)))))
(assert (forall ((A tptp.complex) (B tptp.complex) (C tptp.complex)) (let ((_let_1 (@ tptp.plus_plus_complex A))) (= (= (@ _let_1 B) (@ _let_1 C)) (= B C)))))
(assert (forall ((B tptp.poly_complex) (A tptp.poly_complex) (C tptp.poly_complex)) (= (= (@ (@ tptp.plus_p1547158847omplex B) A) (@ (@ tptp.plus_p1547158847omplex C) A)) (= B C))))
(assert (forall ((B tptp.complex) (A tptp.complex) (C tptp.complex)) (= (= (@ (@ tptp.plus_plus_complex B) A) (@ (@ tptp.plus_plus_complex C) A)) (= B C))))
(assert (not (forall ((C2 tptp.complex)) (not (forall ((W tptp.complex)) (let ((_let_1 (@ tptp.poly_complex2 tptp.pa))) (@ (@ tptp.ord_less_eq_real (@ tptp.real_V638595069omplex (@ _let_1 C2))) (@ tptp.real_V638595069omplex (@ _let_1 W)))))))))
(assert (forall ((N tptp.nat)) (= (@ (@ tptp.ord_less_eq_nat N) tptp.zero_zero_nat) (= N tptp.zero_zero_nat))))
(assert (forall ((N tptp.nat)) (= (not (@ (@ tptp.ord_less_nat tptp.zero_zero_nat) N)) (= N tptp.zero_zero_nat))))
(assert (forall ((X2 tptp.nat) (Y tptp.nat)) (= (= tptp.zero_zero_nat (@ (@ tptp.plus_plus_nat X2) Y)) (and (= X2 tptp.zero_zero_nat) (= Y tptp.zero_zero_nat)))))
(assert (forall ((X2 tptp.nat) (Y tptp.nat)) (= (= (@ (@ tptp.plus_plus_nat X2) Y) tptp.zero_zero_nat) (and (= X2 tptp.zero_zero_nat) (= Y tptp.zero_zero_nat)))))
(assert (forall ((A tptp.poly_poly_complex) (B tptp.poly_poly_complex)) (= (= A (@ (@ tptp.plus_p138939463omplex A) B)) (= B tptp.zero_z1040703943omplex))))
(assert (forall ((A tptp.nat) (B tptp.nat)) (= (= A (@ (@ tptp.plus_plus_nat A) B)) (= B tptp.zero_zero_nat))))
(assert (forall ((A tptp.complex) (B tptp.complex)) (= (= A (@ (@ tptp.plus_plus_complex A) B)) (= B tptp.zero_zero_complex))))
(assert (forall ((A tptp.poly_complex) (B tptp.poly_complex)) (= (= A (@ (@ tptp.plus_p1547158847omplex A) B)) (= B tptp.zero_z1746442943omplex))))
(assert (forall ((A tptp.poly_poly_complex) (B tptp.poly_poly_complex)) (= (= A (@ (@ tptp.plus_p138939463omplex B) A)) (= B tptp.zero_z1040703943omplex))))
(assert (forall ((A tptp.nat) (B tptp.nat)) (= (= A (@ (@ tptp.plus_plus_nat B) A)) (= B tptp.zero_zero_nat))))
(assert (forall ((A tptp.complex) (B tptp.complex)) (= (= A (@ (@ tptp.plus_plus_complex B) A)) (= B tptp.zero_zero_complex))))
(assert (forall ((A tptp.poly_complex) (B tptp.poly_complex)) (= (= A (@ (@ tptp.plus_p1547158847omplex B) A)) (= B tptp.zero_z1746442943omplex))))
(assert (forall ((A tptp.poly_poly_complex) (B tptp.poly_poly_complex)) (= (= (@ (@ tptp.plus_p138939463omplex A) B) A) (= B tptp.zero_z1040703943omplex))))
(assert (forall ((A tptp.nat) (B tptp.nat)) (= (= (@ (@ tptp.plus_plus_nat A) B) A) (= B tptp.zero_zero_nat))))
(assert (forall ((A tptp.complex) (B tptp.complex)) (= (= (@ (@ tptp.plus_plus_complex A) B) A) (= B tptp.zero_zero_complex))))
(assert (forall ((A tptp.poly_complex) (B tptp.poly_complex)) (= (= (@ (@ tptp.plus_p1547158847omplex A) B) A) (= B tptp.zero_z1746442943omplex))))
(assert (forall ((B tptp.poly_poly_complex) (A tptp.poly_poly_complex)) (= (= (@ (@ tptp.plus_p138939463omplex B) A) A) (= B tptp.zero_z1040703943omplex))))
(assert (forall ((B tptp.nat) (A tptp.nat)) (= (= (@ (@ tptp.plus_plus_nat B) A) A) (= B tptp.zero_zero_nat))))
(assert (forall ((B tptp.complex) (A tptp.complex)) (= (= (@ (@ tptp.plus_plus_complex B) A) A) (= B tptp.zero_zero_complex))))
(assert (forall ((B tptp.poly_complex) (A tptp.poly_complex)) (= (= (@ (@ tptp.plus_p1547158847omplex B) A) A) (= B tptp.zero_z1746442943omplex))))
(assert (@ tptp.pp tptp.fTrue))
(assert (not (@ tptp.pp tptp.fFalse)))
(assert (not (exists ((Z2 tptp.complex)) (= (@ (@ tptp.poly_complex2 tptp.pa) Z2) tptp.zero_zero_complex))))
(set-info :filename fta0328.lfho)
(check-sat-assuming ( true ))
